with decls ds dasends on l from e include f(e) and only these for tags in tgs
== (e:E.
== (isrcv(e)
== ( lnk(e) = l
== ( (e':E. isrcv(e') & lnk(e') = l & (tag(e')  tgs) & sender(e') = sender(e))
== ( (tag(e)  tgs))
== & (e':E. isrcv(e')  lnk(e') = l  (tag(e')  tgs)  valtype(e')  da(kind(e'))?Void)
== & (x:Id. vartype(source(l);x)  ds(x)?Top)
== & e@source(l).
== & i:||f(e)||. e':E. isrcv(e') & lnk(e') = l & (tag(e')  tgs) & sender(e') = e & index(e') = i
== & & (e':E.
== & & (isrcv(e')
== & & ( lnk(e') = l
== & & ( (tag(e')  tgs)
== & & ( index(e')<||f(sender(e'))|| & <tag(e'),val(e')> = f(sender(e'))[index(e')]) 

latex

---

clarification:

es-sends-iff(es;l;tgs;da;ds;e.f(e))
== (e:es-E(es).
== (es-isrcv(es; e)
== ( es-lnk(es; e) = l  IdLnk
== ( (e':es-E(es).
== ( (es-isrcv(es; e')
== ( (& es-lnk(es; e') = l  IdLnk
== ( (& & (es-tag(es; e')  tgs  Id)
== ( (& & es-sender(es; e') = es-sender(es; e)  es-E(es))
== ( (es-tag(es; e)  tgs  Id))
== & (e':es-E(es).
== & (es-isrcv(es; e')
== & ( es-lnk(es; e') = l  IdLnk
== & ( (es-tag(es; e')  tgs  Id)
== & ( es-valtype(es; e')  fpf-cap(da;KindDeq;es-kind(es; e');Void))
== & (x:Id. es-vartype(es; source(l); x)  fpf-cap(ds;IdDeq;x;Top))
== & alle-at(es;source(l);e.i:{0..||f(e)||}.
== & e':es-E(es).
== & es-isrcv(es; e')
== & & es-lnk(es; e') = l  IdLnk
== & & (es-tag(es; e')  tgs  Id)
== & & es-sender(es; e') = e  es-E(es)
== & & es-index(es; e') = i  )
== & & (e':es-E(es).
== & & (es-isrcv(es; e')
== & & ( es-lnk(es; e') = l  IdLnk
== & & ( (es-tag(es; e')  tgs  Id)
== & & ( es-index(es; e')<||f(es-sender(es; e'))||
== & & ( & <es-tag(es; e'),es-val(es; e')>
== & & ( & =
== & & ( & f(es-sender(es; e'))[es-index(es; e')]
== & & ( &  tg:Idfpf-cap(da;KindDeq;rcv(l,tg);Void)) 

latex

Definitions	valtype(e), kind(e), vartype(i;x), IdDeq, Top, e@i. P(e), source(l), {i..j}, #$n, x:A. B(x), P & Q, , x:A. B(x), E, b, isrcv(e), IdLnk, lnk(e), P  Q, (x  l), A & B, a<b, ||as||, s = t, x:AB(x), Id, f(x)?z, KindDeq, rcv(l,tg), Void, <a,b>, tag(e), val(e), l[i], index(e), sender(e)
FDL editor aliases	es-sends-iff